import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

public class MyProposition{
	private StringBuilder textPropostion  = null;
	private StringBuilder expressionProposition = null;
	private Map variablesToArrayIndex = null;
	private int[] assignment = null;
	private List assignmentList = null;
	private int countVariables = 0;
	private Map operatorPriority = null;
	private List variablesList = null;
	public List trueAssignment = null;
	public List falseAssignment = null;
	
	private void replaceExp() {
		for(int i=expressionProposition.length()-1; i>=0; i--) {
			switch (expressionProposition.charAt(i)) {
			case '1':
				expressionProposition.setCharAt(i, negation);
				break;
			case '2':
				expressionProposition.setCharAt(i, conjunction);
				break;
			case '3':
				expressionProposition.setCharAt(i, disjunction);
				break;
			case '4':
				expressionProposition.setCharAt(i, implication);
				break;
			case '5':
				expressionProposition.setCharAt(i, biconditional);
				break;
			case ' ':
				expressionProposition.deleteCharAt(i);
			default:
				break;
			}
		}
		System.out.println(expressionProposition);
	}
	
	
	//构造器 暂时只提供通过expressionProposition有参构造
	public MyProposition(String initExp) {
		expressionProposition = new StringBuilder(initExp);
		variablesToArrayIndex = new HashMap();
		String currentVariable = null;
		int arrayIndex = 0;
		variablesList = new ArrayList();
		replaceExp();
		
		//初始化variablesToArrayIndex
		for(int i=0; i<expressionProposition.length(); i++) {
			currentVariable = expressionProposition.substring(i, i+1);
			if(currentVariable.matches("[a-zA-Z]") && !variablesList.contains(currentVariable)) {
				variablesList.add(currentVariable);
			}
			Collections.sort(variablesList);
		}
		for(int i=0; i<variablesList.size(); i++) {
			variablesToArrayIndex.put(variablesList.get(i), i);
		}
		
		//初始化countVariables
		countVariables = variablesToArrayIndex.size();
		
		//初始化assignment
		assignment = new int[countVariables];
		
		//初始化assignmentList
		assignmentList = new ArrayList<String>();
		for(int i=0; i<Math.pow(2, countVariables); i++) {
			assignmentList.add(getBinary(i,countVariables));
		}
		
		//初始化operatorPriority
		operatorPriority = new HashMap();
		operatorPriority.put('(', 0);
		operatorPriority.put(')', 0);
		operatorPriority.put(biconditional, 1);
		operatorPriority.put(implication, 2);
		operatorPriority.put(disjunction, 3);
		operatorPriority.put(conjunction, 4);
		operatorPriority.put(negation, 5);
		
		//初始化真和假
		getTrueAssignment();
		getFalseAssignment();
		
	}
	public List getTrueAssignment() {
		trueAssignment = new ArrayList();
		for(Object s:assignmentList) {
			if(getSingleTruthValue(s.toString())==1) {
				trueAssignment.add(s.toString());
			}
		}
		return trueAssignment;
	}
	
	public List getFalseAssignment() {
		falseAssignment = new ArrayList();
		for(Object s:assignmentList) {
			if(getSingleTruthValue(s.toString())==0) {
				falseAssignment.add(s.toString());
			}
		}
		return falseAssignment;
	}
	
	public String getZHQFS() {
		if(falseAssignment.size()==0) return null;
		StringBuilder sb = new StringBuilder();
		for(Object o : falseAssignment) {
			char[] c = o.toString().toCharArray(); 
			sb.append('(');
			for(int i=0; i<c.length; i++) {
				if(c[i]=='0') {
					sb.append(variablesList.get(i)+String.valueOf(disjunction));
				}else {
					sb.append(String.valueOf(negation)+variablesList.get(i)+String.valueOf(disjunction));
				}
			}
			sb.deleteCharAt(sb.length()-1);
			sb.append(")"+String.valueOf(conjunction));
		}
		if(sb.length()>1) sb.deleteCharAt(sb.length()-1);
		if(!sb.toString().contains(String.valueOf(disjunction))) {
			sb.deleteCharAt(0);
			sb.deleteCharAt(sb.length()-1);
		}
		return sb.toString();
	}
	
	public String getZXQFS() {
		if(trueAssignment.size()==0) return null;
		StringBuilder sb = new StringBuilder();
		for(Object o : trueAssignment) {
			char[] c = o.toString().toCharArray(); 
			sb.append('(');
			for(int i=0; i<c.length; i++) {
				if(c[i]=='1') {
					sb.append(variablesList.get(i)+String.valueOf(conjunction));
				}else {
					sb.append(String.valueOf(negation)+variablesList.get(i)+String.valueOf(conjunction));
				}
			}
			sb.deleteCharAt(sb.length()-1);
			sb.append(")"+String.valueOf(disjunction));
		}
		if(sb.length()>1) sb.deleteCharAt(sb.length()-1);
		if(!sb.toString().contains(String.valueOf(disjunction))) {
			sb.deleteCharAt(0);
			sb.deleteCharAt(sb.length()-1);
		}
		return sb.toString();
	}
	
	//打印真值表
	public void getTruthTable() {
		//1.打印表头
		for(int i=0; i<variablesList.size(); i++) {
			System.out.print(variablesList.get(i)+" ");
		}
		System.out.println(expressionProposition.toString());
		
		//2.打印表身
		for(int i=0; i<assignmentList.size(); i++) {
			for(int j=0; j<assignmentList.get(i).toString().length(); j++) {
				System.out.print(assignmentList.get(i).toString().charAt(j)+" ");
			}

			System.out.println(getSingleTruthValue(assignmentList.get(i).toString()));
		}
	}
	
	
	public int getSingleTruthValue(String assignString) {
//		System.out.println("---------本轮开始---------");
		StringBuilder tempExp = new StringBuilder(expressionProposition);
//		System.out.println(tempExp);System.out.println(variablesToArrayIndex);
		
		//step1: 给所有变量指派01值
		char[] charArray = assignString.toCharArray();
		for(int i=0; i<tempExp.length(); i++) {
			if(tempExp.substring(i, i+1).matches("[a-zA-Z]")) {
				tempExp.setCharAt(i,charArray[(int)variablesToArrayIndex.get(tempExp.substring(i, i+1))]);
//				System.out.println(tempExp.charAt(i));
			}
		}
		
		List operandStack = new ArrayList();
		List operatorStack = new ArrayList();
		
		int i = 0;
		while(i<tempExp.length()) {
			if(tempExp.charAt(i)=='0' || tempExp.charAt(i)=='1') {
				//如果当前读取的是运算数，则把该数压入运算数栈
				operandStack.add(tempExp.charAt(i));
				i++;
			}else if(tempExp.charAt(i)==negation && (tempExp.charAt(i+1)=='0' || tempExp.charAt(i+1)=='1')){
				i++;
//				System.out.println(tempExp.charAt(i)-1-'0');
				tempExp.setCharAt(i, (char) (Math.abs(tempExp.charAt(i)-1-'0')+'0'));
//				System.out.print("i = "+i+"\t");System.out.println(tempExp.charAt(i));
				operandStack.add(tempExp.charAt(i));
				i++;
			}else if(tempExp.charAt(i)==')' && (operatorStack.get(operatorStack.size()-1).toString().equals("("))) {
				operatorStack.remove(operatorStack.size()-1);
				if(operatorStack.size()!=0 && operatorStack.get(operatorStack.size()-1).toString().equals(negation)) {
					operandStack.set(operandStack.size()-1, Math.abs(Integer.parseInt(operandStack.get(operandStack.size()-1).toString())-1));
					operatorStack.remove(operatorStack.size()-1);
				}
				i++;
			}else if(tempExp.charAt(i)=='(') {
				operatorStack.add(tempExp.charAt(i));
				i++;
			}else{

				if(operatorStack.size()==0 || (int)operatorPriority.get(tempExp.charAt(i))>(int)operatorPriority.get(operatorStack.get(operatorStack.size()-1))) {
					//直接压入符号栈
					operatorStack.add(tempExp.charAt(i));
					i++;
				}else {
					//弹出一个操作符和两个运算数，运算后把操作数压入运算数栈
					int b = Integer.parseInt(operandStack.remove(operandStack.size()-1).toString());
					int a = Integer.parseInt(operandStack.remove(operandStack.size()-1).toString());
					char c = (Character)operatorStack.remove(operatorStack.size()-1);
					operandStack.add(getDiadicOperationResult(c, a, b));
				}
				
			}
		
//			System.out.println("---测试1开始---");
//			System.out.println(tempExp);
//			System.out.println("运算数栈："+operandStack);
//			System.out.println("运算符栈："+operatorStack);
//			System.out.println("---测试1结束---");
		}
		while(operandStack.size()!=1) {
			//弹出一个操作符和两个运算数，运算后把操作数压入运算数栈
//			int b = (int)((char)operandStack.remove(operandStack.size()-1)-'0');
//			int a = (int)((char)operandStack.remove(operandStack.size()-1)-'0');
			int b = Integer.parseInt(operandStack.remove(operandStack.size()-1).toString());
			int a = Integer.parseInt(operandStack.remove(operandStack.size()-1).toString());
			char c = (Character)operatorStack.remove(operatorStack.size()-1);
//			System.out.println(a);
//			System.out.println(b);
//			System.out.println(c);
			operandStack.add(getDiadicOperationResult(c, a, b));
			
		}
//		System.out.println("---------本轮结束---------");
//		System.out.println("---测试2开始---");
//		System.out.println(tempExp);
//		System.out.println("运算数栈："+operandStack);
//		System.out.println("运算符栈："+operatorStack);
//		System.out.println("---测试2结束---");
		return (int)operandStack.get(0);
	}
	
	
	public String getBinary(int num, int resLength) {
		StringBuilder binStringBuilder = new StringBuilder();
		while(num!=0) {
			binStringBuilder.insert(0, String.valueOf(num%2));
			num/=2;
			if(binStringBuilder.length()==resLength) break;
		}
		while(binStringBuilder.length()<resLength) {
			binStringBuilder.insert(0, 0);
		}
		return binStringBuilder.toString();
	}
	
	public int getDiadicOperationResult(char operator, int a, int b){
		int res = 0;
		switch (operator) {
		case conjunction:
			if(a==1 && b==1) res = 1;
			else res = 0;
			break;
		case disjunction:
			if(a==0 && b==0) res = 0;
			else res = 1;
			break;
		case implication:
			if(a==1 && b==0) res = 0;
			else res = 1;
			break;
		case biconditional:
			if(a==b) res = 1;
			else res = 0;
			break;
		default:
			break;
		}
		return res;
	}
	
//	private operand
//	private operator
	final char conjunction = '∧';
	final char disjunction = '∨';
	final char negation = '¬';
	final char implication = '→';
	final char biconditional = '↔';
	
	
}
/*
¬
∧
∨
⇒
⇔
*/
